A system of polynomial ordinary differential equations (ode's) is specifiedvia a vector of multivariate polynomials, or vector field, F. A safetyassertion psi->[F]phi means that the system's trajectory will lie in a subsetphi (the postcondition) of the state-space, whenever the initial state belongsto a subset psi (the precondition). We consider the case when phi and psi arealgebraic varieties, that is, zero sets of polynomials. In particular,polynomials specifying the postcondition can be seen as conservation lawsimplied by psi. Checking the validity of algebraic safety assertions is afundamental problem in, for instance, hybrid systems. We consider generalizedversions of this problem, and offer algorithms to: (1) given a user specifiedpolynomial set P and a precondition psi, find the smallest algebraicpostcondition phi including the variety determined by the valid conservationlaws in P (relativized strongest postcondition); (2) given a user specifiedpostcondition phi, find the largest algebraic precondition psi (weakestprecondition). The first algorithm can also be used to find the weakestalgebraic invariant of the system implying all conservation laws in P validunder psi. The effectiveness of these algorithms is demonstrated on a few casestudies from the literature.
展开▼
